computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

, an abstract state machine (ASM) is a

state machine A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...

operating on

states State most commonly refers to: * State (polity), a centralized political organization that regulates law and society within a territory **Sovereign state, a sovereign polity in international law, commonly referred to as a country **Nation state, a ...

that are arbitrary data structures (

structure A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such as ...

in the sense of

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

, that is a nonempty

set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...

together with a number of functions ( operations) and relations over the set).

Overview

The ASM Method is a practical and scientifically well-founded

systems engineering Systems engineering is an interdisciplinary field of engineering and engineering management that focuses on how to design, integrate, and manage complex systems over their Enterprise life cycle, life cycles. At its core, systems engineering uti ...

method that bridges the gap between the two ends of system development: * the human understanding and formulation of real-world problems ( requirements capture by accurate high-level modeling at the level of abstraction determined by the given application domain) * the deployment of their algorithmic solutions by code-executing machines on changing platforms (definition of design decisions, system and implementation details). The method builds upon three basic concepts: * ''ASM'': a precise form of pseudo-code, generalizing

finite-state machine A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...

s to operate over arbitrary data structures * ''ground model'': a rigorous form of blueprints, serving as an authoritative reference model for the design * ''refinement'': a most general scheme for stepwise instantiations of model abstractions to concrete system elements, providing controllable links between the more and more detailed descriptions at the successive stages of system development. In the original conception of ASMs, a single

agent Agent may refer to: Espionage, investigation, and law *, spies or intelligence officers * Law of agency, laws involving a person authorized to act on behalf of another ** Agent of record, a person with a contractual agreement with an insuran ...

executes a program in a sequence of steps, possibly interacting with its environment. This notion was extended to capture distributed computations, in which multiple agents execute their programs concurrently. Since ASMs model algorithms at arbitrary levels of abstraction, they can provide high-level, low-level and mid-level views of a hardware or software design. ASM specifications often consist of a series of ASM models, starting with an abstract ''ground model'' and proceeding to greater levels of detail in successive refinements or coarsenings. Due to the algorithmic and mathematical nature of these three concepts, ASM models and their properties of interest can be analyzed using any rigorous form of verification (by reasoning) or validation (by experimentation, testing model executions).

History

The concept of ASMs is due to

Yuri Gurevich Yuri Gurevich, Professor Emeritus at the University of Michigan, is an American computer scientist and mathematician and the inventor of abstract state machines. Gurevich was born and educated in the Soviet Union. He taught mathematics there and ...

, who first proposed it in the mid-1980s as a way of improving on Turing's thesis that every

algorithm In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...

is simulated by an appropriate

Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...

. He formulated the ''ASM Thesis'': every algorithm, no matter how abstract, is step-for-step emulated by an appropriate ASM. In 2000, Gurevich axiomatized the notion of sequential algorithms, and proved the ASM thesis for them. Roughly stated, the axioms are as follows: * states are structures, * the

state transition In automata theory and sequential logic, a state-transition table is a table showing what state (or states in the case of a nondeterministic finite automaton) a finite-state machine will move to, based on the current state and other inputs. It i ...

involves only a bounded part of the state, and * everything is invariant under isomorphisms of structures. (Structures can be viewed as

algebras In mathematics, an algebra over a field (often simply called an algebra) is a vector space equipped with a bilinear product. Thus, an algebra is an algebraic structure consisting of a set together with operations of multiplication and addition ...

, which explains the original name ''evolving algebras'' for ASMs.) The axiomatization and characterization of sequential algorithms have been extended to parallel and interactive algorithms. In the 1990s, through a community effort, the ASM method was developed, using ASMs for the

formal specification In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...

and analysis (

verification and validation Verification and validation (also abbreviated as V&V) are independent procedures that are used together for checking that a product, service, or system meets requirements and specification (technical standard), specifications and that it fulf ...

) of

computer hardware Computer hardware includes the physical parts of a computer, such as the central processing unit (CPU), random-access memory (RAM), motherboard, computer data storage, graphics card, sound card, and computer case. It includes external devices ...

and

software Software consists of computer programs that instruct the Execution (computing), execution of a computer. Software also includes design documents and specifications. The history of software is closely tied to the development of digital comput ...

. Comprehensive ASM specifications of

programming languages A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their syntax (form) and semantics (meaning), usually defined by a formal language. Languages usually provide features ...

(including

Prolog Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics. Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...

, C, and

Java Java is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea (a part of Pacific Ocean) to the north. With a population of 156.9 million people (including Madura) in mid 2024, proje ...

) and

design language A design language or design vocabulary is an overarching scheme or style that guides the design of a complement of products or architectural settings, creating a coherent design system for styling. Objectives Designers wishing to give their su ...

s ( UML and SDL) have been developed. A detailed historical account can be found elsewhere. A number of software tools for ASM execution and analysis are available.

Publications

Books

* AsmBook: Egon Börger, Robert Stärk
Abstract State Machines: A Method for High-Level System Design and Analysis
* JBook: R.Stärk, J.Schmid, E.Börger
Java and the Java Virtual Machine: Definition, Verification, Validation
* Proceedings/Journal Issues (since 2000) ** 2008: Springer LNCS 523
Abstract State Machines, B and Z
** 2007: J.UCS Special Issue wit
Selected Papers from ASM'07
** 2006: Springer LNCS 511
Rigorous Methods for Software Construction and AnalysisASM and B Dagstuhl Seminar
** 2005: Fundamenta Informatica Special Issue wit

** 2004: Springer LNCS 305
Abstract State Machines 2004
** 2003: Springer LNCS 258
Abstract State Machines 2003: Advances in Theory and Practice
** 2003: TCS special Issue wit
Selected Papers from ASM'03
** 2002: Dagstuhl Seminar Repor
Theory and Applications of Abstract State Machines
** 2001: J.UCS 7.11 Special Issue wit
Selected Papers from ASM'01
** 2000: Springer LNCS 191
Abstract State Machines: Theory and Applications
* Comparative case studies with ASM contributions *
Springer LNCS 1165
*
Production Cell: Software Development Case StudyASM model
*
ASM model
*
Light Control: Requirements Engineering Case StudyDagstuhl Seminar
*
Invoicing: Requirements Capture Case Study

Behavioral models for industrial standards

* OMG for BPMN (version 2006)
Springer LNCS 5316
* OASIS for BPEL
IJBPMI 1.4 (2006)
* ECMA for C#: "A high-level modular definition of the semantics of C♯" * ITU-T for SDL-2000
formal semantics of SDL-2000
an
Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models
* IEEE for VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In: Carlos Delgado Kloos and Peter T.~Breuer (Eds.), ''Formal Semantics for VHDL'', pp. 107–139, Kluwer Academic Publishers, 1995 * ISO for Prolog: "A mathematical definition of full Prolog"

Tools

(in historical order since 2000)
The ASM WorkbenchASMETA, the Abstract State Machine Metamodel and its tool setAsmL
* CoreASM, available a
CoreASM, an extensible ASM execution engine
on Archive.org
The XASM open source project
on

SourceForge SourceForge is a web service founded by Geoffrey B. Jeffery, Tim Perdue, and Drew Streib in November 1999. SourceForge provides a centralized software discovery platform, including an online platform for managing and hosting open-source soft ...

Bibliography

* Y. Gurevich, ''Evolving Algebras 1993: Lipari Guide'', E. Börger (ed.), ''Specification and Validation Methods'',

Oxford University Press Oxford University Press (OUP) is the publishing house of the University of Oxford. It is the largest university press in the world. Its first book was printed in Oxford in 1478, with the Press officially granted the legal right to print books ...

, 1995, 9-36. () * Y. Gurevich, ''Sequential Abstract State Machines capture Sequential Algorithms''
ACM Transactions on Computational Logic
1(1) (July 2000), 77–111. * R. Stärk, J. Schmid and E. Börger, ''Java and the Java Virtual Machine: Definition, Verification, Validation'',

Springer-Verlag Springer Science+Business Media, commonly known as Springer, is a German multinational publishing company of books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing. Originally founded in 1842 in ...

, 2001. () * E. Börger and R. Stärk, ''Abstract State Machines: A Method for High-Level System Design and Analysis'',

, 2003. () * E. Börger and A. Raschke, ''Modeling Companion for Software Practitioners'',

, 2018. (, )

References

External links

Abstract State MachinesAsmCenter

The TASM toolset: specification, simulation, and formal verification of real-time systems
{{DEFAULTSORT:Abstract State Machines Models of computation Formal methods